Skip to content

Remove assess subcommand#4111

Merged
tautschnig merged 6 commits intomodel-checking:mainfrom
carolynzech:remove-assess
Jun 11, 2025
Merged

Remove assess subcommand#4111
tautschnig merged 6 commits intomodel-checking:mainfrom
carolynzech:remove-assess

Conversation

@carolynzech
Copy link
Contributor

@carolynzech carolynzech commented May 27, 2025 •
edited
Loading

Remove assess code and any mentions of it in documentation. This command has been hidden and unused for ~2 years now.

Resolves #1797
Resolves #1798
Resolves #1828
Resolves #1835
Resolves #2053
Resolves #2058
Resolves #2063
Resolves #2099
Resolves #2138
Resolves #2186
Resolves #2294

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Carolyn Zech added 3 commits May 27, 2025 18:29
remove assess
7ab2214
remove dead code
3a279ea
refactor cargokani_main now that assess is gone
91587c5 
We couldn't do this before because of moved value errors, but now that the assess part is gone we can
@carolynzech carolynzech changed the title Remove assess Remove cargo kani assess May 27, 2025
@carolynzech carolynzech changed the title Remove cargo kani assess Remove assess subcommand May 27, 2025
This was referenced May 27, 2025
Open
Open
@carolynzech carolynzech marked this pull request as ready for review May 27, 2025 22:45
@carolynzech carolynzech requested a review from a team as a code owner May 27, 2025 22:45
@carolynzech
Copy link
Contributor Author

carolynzech commented May 27, 2025

cc @celinval

@celinval
Copy link
Contributor

celinval commented May 27, 2025

BTW, you should be able to clean up some of the compiler code as well. You can start by removing this code and all the code that becomes dead after:

kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines 344 to 390 in 7554aef

ReachabilityType::Tests => {
// We're iterating over crate items here, so what we have to codegen is the "test description" containing the
// test closure that we want to execute
// TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
let unit = CodegenUnit::default();
let mut transformer = BodyTransformation::new(&queries, tcx, &unit);
let mut descriptions = vec![];
let harnesses = filter_const_crate_items(tcx, &mut transformer, |_, item| {
if is_test_harness_description(tcx, item.def) {
descriptions.push(item.def);
true
} else {
false
}
});
// Codegen still takes a considerable amount, thus, we only generate one model for
// all harnesses and copy them for each harness.
// We will be able to remove this once we optimize all calls to CBMC utilities.
// https://github.com/model-checking/kani/issues/1971
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items, contract_info) = self.codegen_items(
tcx,
&harnesses,
&model_path,
&results.machine_model,
Default::default(),
transformer,
);
results.extend(gcx, items, None);
assert!(contract_info.is_none());
for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
let instance =
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
let metadata = gen_test_metadata(tcx, *test_desc, *instance, base_filename);
let test_model_path = &metadata.goto_file.as_ref().unwrap();
std::fs::copy(&model_path, test_model_path).unwrap_or_else(|_| {
panic!(
"Failed to copy {} to {}",
model_path.display(),
test_model_path.display()
)
});
results.harnesses.push(metadata);
}
}

@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label May 27, 2025
celinval
celinval approved these changes May 29, 2025
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not my call, but I just got excited about this clean up. 😊

@tautschnig tautschnig added this pull request to the merge queue Jun 11, 2025
Merged via the queue into model-checking:main with commit 5b6700e Jun 11, 2025
25 of 26 checks passed
@carolynzech carolynzech deleted the remove-assess branch June 11, 2025 13:30
@carolynzech carolynzech mentioned this pull request Jul 3, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jul 3, 2025
Bump Kani version to 0.64.0 (#4198)
96f7e59 
Auto generated release notes:

## What's Changed
* Edit quantifiers' documentation. by @thanhnguyen-aws in
#4142
* Fix the bug of using multiple hidden variables for the prev of the
same Expr by @thanhnguyen-aws in
#4150
* Remove `assess` subcommand by @carolynzech in
#4111
* Optimize goto binary exporting in `cprover_bindings` by
@AlexanderPortland in #4148
* Add the option to generate performance flamegraphs by
@AlexanderPortland in #4138
* Fix the bug: Static union values can panic Kani by @thanhnguyen-aws in
#4112
* Update toolchain to 2025-06-13 by @carolynzech in
#4152
* Automatic cargo update to 2025-06-16 by @github-actions in
#4156
* Major-version update cargo dependencies by @tautschnig in
#4158
* Upgrade Rust toolchain to 2025-06-16 by @tautschnig in
#4157
* Bump tests/perf/s2n-quic from `3129ad5` to `c6e694e` by @dependabot in
#4160
* Bump tests/perf/s2n-quic from `c6e694e` to `b1b5bf8` by @dependabot in
#4164
* Upgrade Rust toolchain to 2025-06-17 by @tautschnig in
#4163
* Automatic cargo update to 2025-06-23 by @github-actions in
#4172
* Stub panics during MIR transformation by @AlexanderPortland in
#4169
* Bump tests/perf/s2n-quic from `b1b5bf8` to `32ba87d` by @dependabot in
#4175
* Handle enums with zero or one variants by @zhassan-aws in
#4171
* Introduce compiler timing script & CI job by @AlexanderPortland in
#4154
* Upgrade Rust toolchain to 2025-06-18 by @tautschnig in
#4166
* Cache dependencies for CI jobs by @AlexanderPortland in
#4181
* Autoharness: Derive `Arbitrary` for structs and enums by @carolynzech
in #4167
* Upgrade Rust toolchain to 2025-06-27 by @tautschnig in
#4182
* Include wget in dependencies by @zhassan-aws in
#4183
* Automatic cargo update to 2025-06-30 by @github-actions in
#4186
* Add support for loop assigns in loop contracts by @thanhnguyen-aws in
#4174
* Upgrade toolchain to 06/30 by @carolynzech in
#4188
* Optimize reachability with non-mutating global passes by
@AlexanderPortland in #4177
* Bump tests/perf/s2n-quic from `32ba87d` to `b8f8cca` by @dependabot in
#4190
* Bump ncipollo/release-action from 1.16.0 to 1.18.0 by @dependabot in
#4191
* Upgrade toolchain to 07/02 by @carolynzech in
#4195
* Automatic Derivation Fixes by @carolynzech in
#4194


**Full Changelog**:
kani-0.63.0...kani-0.64.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment